\chapter{数据平面验证与网络协同应用编程的抽象和流程}
\label{cha:overview}
本章对数据平面验证与网络协同应用编程的基本抽象和主要流程进行抽象化描述，首先对网络验证和编程所涉及的对象进行形式化描述，然后基于抽象描述介绍网络验证和编程的基本流程，为后续章节的研究工作提供重要的基础和理论支持。


\section{数据平面验证与网络协同应用编程的基本抽象}
实现网络验证和网络协同应用编程的前提是深入了解网络涉及的基本对象及其交互过程，这就需要对网络相关元素进行形式化描述，并建立其抽象模型。
% 同时，对数据平面进行验证的前提是需要深入理解网络的工作原理和流程，这就要求对数据平面的静态结构和动态行为有充分的分析。数据平面负责数据包转发的部分，主要由物理网络拓扑和设备的转发信息表定义，这两个组成部分共同决定了整个网络的数据包转发行为。因此，对数据平面进行形式化描述是非常必要的。

\subsection{网络拓扑抽象}
一个物理网络包含多个设备，设备之间通过物理链路连接，由于任意两个设备之间可能存在多条物理链路，且对于任意一条链路，不同的数据传输方向具有不同的特性（如：带宽、延迟和权重等），所以网络拓扑可以抽象为一个有向多边图 (Directed multigraph) $G(D,L)$，其中$D$为所有网络设备和终端主机集合，符号$term(D) \subseteq D$表示所有的终端设备，$net(D) \subseteq D$表示所有的网络设备（如：路由器和交换机），终端设备负责产生和接收数据包，网络设备负责转发数据包。

每个设备$d \in D$具有多个物理端口$\Psi_d=\{\psi_1^d,...,\psi_{|\Psi_d|}^d\}$，其中$\psi_i^d$表示设备$d$的第$i$个端口。令$\Omega=\bigcup_{d \in D}\Psi_d$为网络中所有端口集合, 则$L \subseteq \Omega \times \Omega$为该有向多边图$G$的边集合，每条有向边$(\psi^u_i, \psi^v_j) \in L$表示网络中存在一条从设备$u$的第$i$个端口到设备$v$的第$j$个端口的链路，由于本文针对的链路为全双工链路，所以$|L|$为偶数，换言之，如果$(\psi^u_i, \psi^v_j) \in L$，则$(\psi^v_j, \psi^u_i) \in L$。在上下文清楚的情况下，本文用$\psi$表示一个端口。

另外，本文用$dev(\psi)$表示端口$\psi$所属的设备，$peer(\psi)$表示与端口$\psi$连接的对端端口，$pdev(\psi) = dev(peer(\psi))$表示对端端口所属的设备。对于一条链路$l=(\psi_i, \psi_j) \in L$，本文用$src(l) = \psi_i$和$dst(l) = \psi_j$分别表示有向边$l$的开始和结束端口，$srcd(l) = dev(\psi_i)$和$dstd(l) = dev(\psi_j)$表示$l$所连接的开始和结束设备。

\subsection{网络路径抽象}
\begin{definition}
  \textbf{网络路径($\pi$)。} 一个网络路径$\pi$为一个网络链路构成的有序序列$\pi = \{l_1, l_2,...,l_N\}$，其中$l_i \in L$，$N$为该路径长度，且相邻链路必须连接到同一个设备以保证路径连通，即$\forall i \in [1, N-1]: dstd(l_i) = srcd(l_{i + 1})$。
\end{definition}

需要指出的是，如果$srcd(l_1) \in term(D)$且$dstd(l_N) \in term(D)$，本文称路径$\pi$是一条端到端的路径（End-to-end path）。如果网络中不存在多链路（multi-link）情况，网络路径可以等价的表示为一个设备有序序列$\pi=\{d_1,d_2,...,d_N\}$，其中$d_i = dstd(l_i)$，从而能够更精简地表达一个路径。另外，本文用$\Pi \subseteq L^*$表示网络中的路径集合。

% 一个网络路径$\pi$为一个物理端口构成的有序序列$\{\psi_1,\psi_2,...,\psi_N\}$，其中$\psi_i \in \Omega$，$N$为该路径长度。
% \begin{definition}
%   \textbf{有效网络路径（Valid path）}。本文称网络路径$\pi$是有效的（valid）当且仅当1) 路径连通，即$\forall i \in [1, N -1]: pdev(\psi_i) = dev(\psi_{i+1})$；2）路径无环，即$\forall i,j \in [1, N - 1]: dev(port_i) \neq dev(port_j)$。
% \end{definition}

% 特别地，如果$port_1 \in term(D)$且$port_N \in term(D)$，本文称路径$\pi$是一条端到端的路径（End-to-end path）。如果网络中不存在多链路（multi-link）情况，网络路径可以等价的表示为一个设备有序序列$\pi=\{d_1,d_2,...,d_N\}$，其中$d_i = pdev(port_i)$，从而能够更精简地表达一个路径。本文用$\Pi$表示网络中所有的有效路径集合。
% 一个网络路径$Path$为一个网络设备有序序列$Path=\{d_1,d_2,...,d_N\}$，本文称网络路径$Path$是有效的（valid）当且仅当$\forall i \in [1, N -1]:$ $d_i$和$d_j$之间存在物理连接。

\subsection{网络数据包抽象}
网络数据包由一个数据包头$h$和数据包内容构成，本文主要关注网络数据包头，定义数据包头如下：
\begin{definition}
  \textbf{数据包头($h$)：}一个数据包具有一个固定长度的比特序列数据包头$h \in \{0,1\}^{|h|}$，其中$|h|$为数据包头长度。
\end{definition}

由于网络往往根据特定的路由协议工作，路由协议只关心其对应数据包头的某一部分，在没有特别说明情况下，本文中的数据包头指代路由协议相关部分，比如在一个基于目的IP地址转发的IPv4路由网络中，目的地址为1.2.3.4的数据包头为$h=\{00000001\ 00000010\ 00000011\ 00000100\}$，本文用$\mathcal{L}$来表示协议对应的数据包头长度，如基于目的IP地址转发的IPv4路由网络中$\mathcal{L}=32$。同时，本文用符号$\mathbb{H}$表示协议所能表达的所有的数据包头集合，如在一个IPv4路由网络中，$\mathbb{H} = \{0,1\}^{32}$。为了简化表示，在上下文清楚的情况下，本文也使用IP地址来表示一个数据包头（如10.0.0.1）。



\begin{definition}
  \textbf{包头空间($H$)：}多个数据包头的集合构成一个包头空间$H=\{h_1,...,h_{|H|}\}$，其中$|H|$为该包头空间包含的数据包头数量，且$\forall i \neq j: h_i \neq h_j$。
\end{definition}

在IP路由网络中，网络通常会划分为多个子网，子网用IP地址和子网掩码构成，网络设备也通常用IP prefix来定义路由规则，而一个IP prefix定义了一个包头空间，如IPv4地址前缀10.0.0.0/24对应于一个包含$2^8$个数据包头的包头空间$\{10.0.0.0,...,10.0.0.255\}$。另外，定义函数$H(h): \mathbb{H} \rightarrow Bool$表示数据包头$h$是否存在于包头空间$H$。为了简化表示，在上下文清楚的情况下，本文也使用IP地址前缀来表示一个包头空间（如10.0.0.0/24）。

% \todo{h -> H}
% \todo{move to dpg}
% \begin{definition}
%   \textbf{无冲突数据平面需求（Conflict-free DPR）。}给定两个数据平面需求$\rho_i=\langle d_i, h_i, \pi_i \rangle$和$\rho_j=\langle d_j, h_j, \pi_j \rangle$，如果$h_i = h_j$，且$\exists port_i \in \pi_i, port_j \in \pi_j: port_i \neq port_j, dev(port_i) = dev(port_j)$，则$\rho_i$和$\rho_j$是冲突的，否则他们是无冲突数据平面需求。
% \end{definition}

% \todo{fix it}
% \subsection{应用逻辑抽象}
% 一个应用程序的逻辑可能会相当复杂，由于本文主要关心的是其与网络传输相关的部分，所以本文所涉及的应用主要指代与网络编程中数据发送部分。本文用AF(Application function)来表示应用逻辑，其定义为$AF: M \times \mathbb{N} \rightarrow \mathbb{H}$，其中$M$表示应用自身的状态数据，$\mathbb{N}$为网络拓扑，$\mathbb{H}$为产生的数据流包头。

% \subsection{网络控制抽象}
% 网络控制主要根据应用需求将应用产生的数据流与数据平面需求进行绑定，本文用NF(Network function)来表示网络控制逻辑，其定义为$NF: \mathbb{H} \times \mathbb{N} \rightarrow \mathbb{H} \times \Pi$。

% \subsection{网络控制和应用逻辑的关系模型}

% \subsection{数据平面验证基本抽象}

\subsection{数据平面行为抽象}
网络的数据平面决定了网络设备如何处理进入网络的数据包。具体来说，给定一个物理网络$G(D,L)$, 每个网络设备$d \in net(D)$包含一套转发信息表（FIB）$R_d$，其中包含一系列数据包转发规则$R_d = \{r_1,...,r_{|T_d|}\}$，每条规则$r\in R_d$可抽象为一个三元组$\langle pri_r, match_r, action_r \rangle$（为了精简表达，在上下文清楚的情况下，本文也使用$\langle pri_r, m_r, a_r\rangle$表示规则元素）, 其中$pri_r \in \mathbb{Z}$为该规则的优先级（本文约定$pri_r$越大优先级越高），$m_r \in \{0,1,\text{x}\}^\mathcal{L}$为数据包头的匹配值，x为任意匹配，$a_r$为对应的动作，如转发、多播、广播或者丢弃。FIB的语义如下，对于进入网络设备$d$的具有包头为$h$的数据包，对于规则$r \in R_d$，如果$m_r$域能够匹配$h$，且$pri_r$是匹配$h$的最高优先级规则，则使用规则$a_r$来处理该数据。为了精简表达，在上下文清楚的情况下，本文也使用$field=val$列表来表示一个match域（如$m_r := [dstIP=10.0.0.0/24]$）。

% 网络的数据平面决定了网络设备如何处理进入网络的数据包。具体来说，当一个数据包进入一个网络设备$u$，该设备会根据数据包头内容将数据包转发到相应端口$\psi_u^i$，同时也可能对该数据包进行修改，如果该端口连接到另一个网络设备，即$\exists (\psi_u^i, \psi_v^j) \in E$，则数据包进一步会被设备$v$用同样的方式处理。本小节对上述过程进行形式化描述。

% \subsubsection{数据平面的布尔逻辑抽象}
% \begin{definition}
%   数据包头(packet header)：一个数据包具有一个固定长度的比特序列数据包头$h=\{b_1,...,b_{|h|}\}$，其中$b_i \in \{0,1\}$，$|h|$为该比特序列的长度。
% \end{definition}

% 由于网络往往根据特定的路由协议工作，路由协议只关心其对应数据包头的某一部分，在没有特别说明情况下，本文中的数据包头指代协议相关部分，比如在一个基于目的IP地址转发的IP路由网络中，目的地址为1.2.3.4的数据包头为$h=\{00000001\ 00000010\ 00000011\ 00000100\}$。另外，本文用$\mathbb{H}$表示所有的数据包头集合。

% \begin{definition}
%   包头空间(header space)：多个数据包头的集合构成一个包头空间$H=\{h_1,...,h_{|H|}\}$，其中$|H|$为该包头空间包含的数据包头数量，且$\forall i \neq j: h_i \neq h_j$。
% \end{definition}

% 在IP路由网络中，网络通常会划分为多个子网，子网用IP地址和子网掩码构成，网络设备也通常用IP prefix来定义路由规则，而一个IP prefix定义了一个包头空间，如IPv4地址前缀10.0.0.0/24对应于一个包含$2^8$个数据包头的包头空间$\{10.0.0.0,...,10.0.0.255\}$。另外，本文定义函数$H(h): \mathbb{H} \rightarrow Bool$表示数据包头$h$是否存在于包头空间$H$。

\textbf{单个网络设备数据平面的行为抽象。}给定一个网络设备$d$，对于一条转发规则$r \in R_d$，$m_r$本质上是一个包头空间，如基于目的IP的路由为了中，$m_r := [dstIP=10.0.0.0/24]$对应于包头空间$H_r = \{10.0.0.0,...,10.0.0.255\}$。另外，$a_r$决定了数据包的处理，如$a_r := forward(eth0)$表示将数据包转发到eth0。基于上述抽象，一个网络设备基于其转发信息表$R_d$处理数据包的过程可以抽象为一个函数$F_d: \mathbb{H} \rightarrow A_d$，其中$A_d=\{a_r|r \in R_d\}$为$R_d$所有action的集合，定义如下：

\begin{equation}
  F_d(h) = a_r, \text{其中}r = \mathop{\arg\max}\limits_{H_r(h)=True, r \in R_d}pri_r
\end{equation}

\textbf{整体网络数据平面的行为抽象。}基于单个设备的数据平面行为抽象，整体网络数据平面的行为可抽象为一个迭代函数。本文定义整体网络数据平面的行为如下：

\begin{equation}
  \mathcal{F}_\mathcal{R}(d, h) = \{F_{d_1}(h), F_{d_2}(h),...,F_{d_N}(h)\}
\end{equation}
其中$\mathcal{R}$为所有设备的数据平面配置集合，且$d_i = pdev(F_{d_{i-1}}(h)), i \in [1,N]$。$\mathcal{F}_\mathcal{R}(d, h)$表示给定数据平面配置$\mathcal{R}$，当数据包头为$h$的数据包通过设备$d$进入网络时，$\mathcal{F}_\mathcal{R}$返回数据包经过设备的匹配规则的动作集合。如果不指定初始设备$d$，$\mathcal{F}$返回所有网络设备对于包头$h$的动作，网络的整体行为定义为：

\begin{equation}
  \mathcal{F}(h, \mathcal{R}) = \{F_{d}(h) | d \in net(D)\}
\end{equation}



\subsection{数据平面需求抽象}
网络协同应用编程需要应用对网络所需实现的功能进行描述，即网络应该如何处理应用产生的数据流，本文将其称为数据平面需求。
\begin{definition}
  \textbf{数据平面需求（$\rho$）。} 数据平面需求为一个元组$\rho = \langle d, h, \pi \rangle$，其中$d \in term(D)$为一个网络设备，$h$为一个数据包头，$\pi=\{l_1,...,l_N\}$为一条网络路径，且$d = srcd(l_1)$。
\end{definition}

对于一个数据平面需求$\rho = \langle d, h, \pi \rangle$，其语义为从设备$d$出发且包头为$h$的数据包，网络需要按照路径$\pi$对该数据包进行转发。

值得注意的是，已有工作如Merlin~\cite{soule2014merlin}和Propane~\cite{beckett2016don}等使用正则表达式方式表示路径需求，对于正则形式路径的需求依然可以等价的表示为多个满足正则条件的路径，上述数据平面需求抽象仍然可以作为基础结构表示这些需求。在本文实际系统中，也使用正则形式的路径需求，但并不打破上述数据平面需求抽象的定义。

% \begin{definition}
%   数据包头($h$)：一个数据包包含一个具有固定长度的比特序列包头$\{b_1,...,b_n\}$，其中$b_i \in \{0, 1\}$。 本文将其抽象为一个布尔变量序列$h=\{x_1,...,x_n\}$，其中布尔变量$x_i := (b_i = 1)$。
% \end{definition}

% 一个数据包头$h$可以根据数据包转发协议进行分组，如源IP地址，目的IP地址等。则$h=\{field_1,...field_n\}$，其中$field_i$表示数据包头的第$i$组布尔变量。

% \begin{definition}
%   包头空间($H$)：包含多个数据包头的集合$\{h_1,...,h_k\}$构成一个包头空间，本文将包头空间抽象为其所包含的所有数据包头的析取$H=\vee_i^k h_i$。
% \end{definition}

% 令$\{x_1,...x_n\}$为一个布尔变量集合，对于一个数据包头$h=\{b_1,...,b_n\}$，本文将其表示为一个布尔逻辑表达式$p_h = c_1 \wedge c_2 ... \wedge c_n$ （简写为$c_1c_2...c_n$），其中：

% \begin{equation}
%   c_i = \begin{cases}
%     x_i & b_i = 1 \\
%     \bar{x_i} & b_i = 0
%   \end{cases}
% \end{equation}
% 例如，数据包头 1010 表示为布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4}$。

% 与之相应，包头空间$H=\{h_1,...h_k\}$的布尔逻辑表达式为$p_H = \vee_{i=1}^k p_{h_i}$。例如，数据包头 1010 和 1011 构成的包头空间布尔逻辑表达式为$x_1\bar{x_2}x_3\bar{x_4} \vee x_1\bar{x_2}x_3x_4 = x_1\bar{x_2}x_3$。给定一个数据包头，本文可以很容易根据该数据包头生成布尔表达式的变量值，进而验证该数据包头是否满足一个布尔表达式，所以本文也将上述布尔表达式称为\textbf{谓词} (predicates)。所以，一个predicate $p$对应于一个包头空间$\{h | p(h) = True, \forall h \in \mathbb{H}\}$。


% 网络设备$d \in D$的FIB抽象为一个三元组集合$F_d = \{(pri_1, H_1, a_1),...,(pri_n, H_n, a_n)\}$，令$F: D \times \mathbb{H} \rightarrow A$ 为数据平面转发函数，给定一个数据包头$h$，其定义如下：
% \begin{equation}
%   F(d, h) = a_k^d, \text{其中}k = \mathop{\arg\max}\limits_{H_k^d(h)=True}pri^d_k
% \end{equation}




\section{数据平面验证与网络协同应用编程的基本流程}
% \subsection{网络协同应用编程的基本流程}
基于前面章节对数据平面验证与网络协同应用编程所涉及对象的形式化描述，可以精简的表达数据平面验证与网络协同应用编程的基本流程。\cref{fig:overview-workflow}所示为数据平面验证与网络协同应用编程的基本流程，整体包括以下模块：

\begin{figure}[]
  \centering
  \includegraphics[width=0.78\linewidth]{figures/overview/workflow.pdf}
  \caption{数据平面验证与网络协同应用编程的基本流程}
  \label{fig:overview-workflow}
\end{figure}

\begin{enumerate}
  \item \textbf{数据平面模型构建：}数据平面模型构建主要是建立易于验证的与数据平面配置等价的模型结构。通过对收集到的网络设备FIB更新进行综合处理（如计算原子谓词~\cite{yang2016realtime}），形成如有向图等易于计算机快速处理的数据平面模型。
  \item \textbf{网络需求验证：}网络需求验证主要在数据平面模型上运行相应的验证算法从而实现网络需求验证。例如，对于图结构的数据平面模型，验证算法可通过图遍历方式来验证可达性需求，对于SMT结构的数据平面模型，则可以通过求解SMT约束实现验证。
  \item \textbf{网络协同应用编程：}网络协同应用编程为运行在终端设备上的基于网络协同应用编程框架的应用程序，通过框架提供的编程API和编程模型实现网络控制和应用逻辑的结合。
  % \item \textbf{NAI 程序：} NAI 程序为运行在终端设备上的基于网络协同应用编程框架的应用程序，框架基于网络状态和应用需求计算相应的数据平面需求，并可以基于网络状态动态调整应用逻辑。
  \item \textbf{数据平面配置生成：} 数据平面配置生成接收所有网络协同应用程序的数据平面需求，并生成满足所有应用需求的数据平面配置。最后通过控制平面协议（如：Openflow）将配置下发到网络设备。
  % \item \textbf{数据平面验证器：} 数据平面验证器获取所有网络设备的FIB以及NAI程序的数据平面需求，然后验证当前数据平面是否能满足数据平面需求，最后将验证结果反馈给NAI程序。
\end{enumerate}

各个模块之间通过以下步骤完成网络协同应用与验证的过程：\circled{1} 数据平面验证器监听数据平面FIB的变化$\{\Delta R_1,...,\Delta R_{|net(D)|}\}$，并更新相应的数据平面模型；\circled{2} 当数据平面模型发生变化时，在数据平面模型上对数据平面需求进行验证；\circled{3} 验证结果$\{z_1,...,z_N\}$ 可以被上层应用程序使用，如发送给应用程序，应用程序可以根据验证器的结果进一步调整应用逻辑。在网络协同应用方面，\circled{4} 网络协同应用编程输出网络需求路径集合$\{\pi_1,...,\pi_N\}$，并将其输入到数据平面配置生成系统；\circled{5} 数据平面配置生成器根据路径和数据包头生成各个网络设备的数据平面配置$\{R_1,...,R_{|net(D)|}\}$，并通过控制平面协议下发到各个网络设备；同时，\circled{6} 数据平面配置生成过程将收到数据平面需求集合后，生成每个数据平面需求路径对应的数据包头$\{h_1,...,h_N\}$，并发送给应用程序；\circled{7} 应用程序基于数据平面配置生成过程反馈的数据包头对应用发出的数据包头进行调整，并生成修改后的数据平面配置$\{\rho_1,...,\rho_N\}$，将其发送给数据平面验证系统进行验证。

% 各个模块之间通过以下步骤完成网络协同应用与验证的过程：\circled{1} NAI 程序向验证器请求网络状态信息$G(N,L)$，作为应用程序的状态变量；\circled{2} NAI 程序结合网络状态和应用需求输出数据平面需求集合$\{\rho_1,...,\rho_N\}$，并发送给数据平面配置生成器；\circled{3} 数据平面配置生成器收到数据平面需求集合后，对数据平面需求进行冲突分析，并生成每个数据平面需求对应的无冲突数据包头$\{h_1,...,h_N\}$，并发送给NAI程序；\circled{4} 数据平面配置生成器根据路径和数据包头生成各个网络设备的数据平面配置$\{T_1,...,T_{|net(d)|}\}$，并通过控制平面协议下发到各个网络设备；\circled{5} NAI 程序基于数据平面配置生成器反馈的无冲突数据包头替换原始数据平面需求的数据包头，生成修改后的数据平面配置$\{\rho_1',...,\rho_N'\}$，并发送给数据平面验证器；\circled{6} 数据平面验证器监听数据平面FIB的变化$\{\Delta T_1,...,\Delta T_{|net(D)|}\}$，并更新相应的数据平面模型，在数据平面模型上对数据平面需求进行验证；\circled{7} 验证结果$\{z_1,...,z_N\}$ 发送给NAI程序，NAI程序可以根据验证器的结果进一步调整应用逻辑。


% \subsection{数据平面验证的基本流程}
% 数据平面验证的主要流程如图~\ref{fig:dpv-workflow}所示。首先，数据平面验证系统收集网络设备的转发信息表及其更新（FIB snapshot/update），然后构建相应的数据平面模型（data plane model），该模型将网络抽象为一个带有边标签的有向图$G(V, E, L)$，其中$V$为所有网络设备，有向边$e=(u,v)\in E$表示从设备$u$到设备$v$的链路, 令$src(e)=u, dst(e)=v$分别表示边$e$的起始和目标节点，$(e, H) \in L$表示设备$src(e)$的FIB将属于数据包头空间$H$的数据包通过链路$e$转发到$dst(e)$。数据平面验证系统接收用户对网络的正确性需求（Requirement），然后在数据平面模型上应用相应的图算法对需求的可满足性进行验证，最终输出验证结果（Verification results）。

% \begin{figure}[htbp]
%   \centering
%   \includegraphics[width=0.8\textwidth]{dpv-workflow.pdf}
%   \caption{数据平面验证基本流程}
%   \label{fig:dpv-workflow}
% \end{figure}

% \section{网络协同应用编程与验证的关键挑战}
% \subsection{网络协同应用编程的挑战}
% 网络协同应用编程主要包括以下关键挑战：
% \begin{enumerate}
%   \item 如何设计网络协同应用的编程模型，通过相应的数据结构和接口实现网络控制和应用逻辑调整相结合。
%   \item 对于网络中所有的数据平面需求，如何生成正确且最优的数据平面配置。
% \end{enumerate}

% \subsection{数据平面验证的挑战}
% 数据平面验证主要包括以下关键挑战：
% \begin{enumerate}
%   \item 如何实现快速实时的数据平面模型构建？
%   \item 如何在不完整的数据平面模型上实现一致性验证？
% \end{enumerate}

% \section{网络协同应用编程与验证的挑战}
% \subsection{网络协同应用编程的关键的挑战}

% \subsection{数据平面验证的挑战}
% 根据上述数据平面验证流程，数据平面验证主要需要解决以下关键问题：

% \subsubsection{数据平面模型构建问题}

% \subsubsection{数据平面验证一致性问题}
% \begin{enumerate}
%   \item 如何保证数据平面模型与数据平面状态一致
%   \item 何时进行验证
% \end{enumerate}

% \subsubsection{数据平面快速增量式验证问题}

% \subsubsection{数据平面验证扩展性问题}

% \begin{enumerate}
%   \item 如何基于收集到的FIB构建有利于高效验证的数据平面模型。
%   \item 基于数据平面模型如何实现快速且一致的验证。
%   \item 针对大规模网络，如何实现具有高扩展性的分布式数据平面验证。
% \end{enumerate}

% \section{数据平面验证与网络协同应用编程的研究内容}

% 基于数据平面验证与网络协同应用编程的基本流程，针对流程中的四个关键模块，本文分别展开了以下研究：

% \begin{enumerate}
%   \item \textbf{面向大规模网络的数据平面模型构建研究。}数据平面模型是描述数据平面行为且易于实现验证的抽象结构，其构建速度直接关系到验证系统的效率。在大规模网络下，大量的FIB更新意味着计算量的增加，进而使数据平面模型更新迟滞，因此，本文进行了“面向大规模网络的数据平面模型构建研究”（\cref{cha:model}），以实现大规模网络下的数据平面模型高效构建。
%   \item \textbf{面向大规模网络的数据平面一致性快速验证研究。}网络需求的验证以数据平面模型作为输入，而FIB收集的异步性可能导致数据平面模型与真实网络不一致，进而得出不一致的验证结果，同时验证算法也需要能够在不断更新的数据平面模型上实现增量式验证以提高验证速度。因此，本文进行了“面向大规模网络的数据平面一致性快速验证研究”（\cref{cha:consistency}），以实现大规模网络下的一致性验证和增量式验证。
%   \item \textbf{面向网络协同应用编程的编程框架研究。}实现网络协同应用编程的关键在于提供一套灵活的编程框架，通过制定相应的编程模型，以及相应的数据结构和函数模板来统一网络控制和应用逻辑编程，一方面能够简化网络协同应用的编程难度，另一方面能够规范程序结构。因此，本文进行了“面向网络协同应用编程的编程框架研究”（\cref{cha:socker}），旨在提供灵活易用的网络协同应用编程框架。
%   \item \textbf{面向网络协同应用编程的数据平面配置生成研究。}面向网络协同应用编程需要能够在网络的数据平面层面满足应用需求，而数据平面行为是由FIB决定的，所以需要相应的数据平面配置生成系统来生成满足应用需求的FIB。因此，本文进行了“面向网络协同应用编程的数据平面配置生成研究”（\cref{cha:dpg}），以实现网络协同应用编程过程中数据平面配置的生成。
% \end{enumerate}

\section{本章小结}
本章对数据平面验证与网络协同应用编程的基本抽象和主要流程进行描述。首先对数据平面验证与网络协同应用编程所涉及的对象进行了形式化的定义，然后介绍了数据平面验证与网络协同应用编程的核心流程。这些抽象和流程的介绍将为后续章节的研究工作提供重要的理论基础和方法论指导。